Nuprl Lemma : append_nil_sq
11,40
postcript
pdf
l
:(top List). sqequal(append(
l
; []);
l
)
latex
Definitions
t
T
,
Y
,
append(
as
;
bs
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
l:(top List). sqequal(append(l; []); l) l:(top List). sqequal(append(l; []); l) 
Tx:A. B(x)